M:MsgA, a:Id. a in dom(M.pre)   

latex

Definitions	x:A. B(x), t  T, , a in dom(M.pre), t.1, t.2, x. t(x), MsgA, x(s)
Lemmas	assert wf, fpf-dom wf, Id wf, id-deq wf, fpf-trivial-subtype-top, ma-state wf, bool wf, msga wf